/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.semantic;

import java.util.Iterator;
import java.util.List;

import alloy.ast.Module;
import alloy.ast.ModuleInfo;
import alloy.ast.QualifiedName;
import alloy.ast.SigExpr;
import alloy.ast.SigExprs;
import alloy.ast.Signature;
import alloy.type.SigType;
import alloy.type.UnionType;
import alloy.util.Dbg;
import alloy.util.Msg;

/**
 * creates SigTypes for all sigs in the spec
 */

public class SigTypeCreator {

    // the module info for the focus module
    private ModuleInfo _moduleInfo;

    // cannot be instantiated
    private SigTypeCreator() {}

    /**
     * creates signature types for all given sigs
     * @param sigs_ the sigs, sorted so that
     *              no sig appears before a sig it extends
     * @param moduleInfo_ the ModuleInfo for the focus module
     */
    public static void createSigTypes(List sigs_, ModuleInfo moduleInfo_) {

	// initialize SigType tables
        SigType.init();
	Iterator sigIter = sigs_.iterator();
	// determine the types of all signatures
	
	while (sigIter.hasNext()) {
	    Signature sig = (Signature) sigIter.next();
	    _createTypeForSig(sig, moduleInfo_);
	    if (sig.getUnionType()==null) { // could not type it, an error ocurred
	        return;
	    }
	}

	//_displayTypeInfo(sigs_);
	
    }

    /** 
     * Prints out sig type info to the console
     * @param sigs_ the list of typed signatures
     **/
    private static void _displayTypeInfo(List sigs_) {
	Iterator sigIter = sigs_.iterator();
	while (sigIter.hasNext()) {
	    Signature sig = (Signature) sigIter.next();
	    System.out.println(sig);
	    if (!sig.isSubset()) {
		System.out.println("  type: " + sig.getSigType());
	    
		System.out.print("  subtypes: ");
		Iterator children = sig.getSigType().getSubTypes().iterator();
		while (children.hasNext())
		    System.out.print(((SigType) children.next())+" ");
	    
		System.out.print("\n");
		
		System.out.println("  supertype: " + sig.getSigType().getSuperType());
	    } else {
		System.out.println("  type: " + sig.getUnionType());
	    }

	}
    }


    /**
     * Creates UnionType for sig_.  This method checks that no
     * sig extends a subset.  It also assigns types to the SigExprs that
     * represent Signatures which sig_ extends or subsets.
     * @param sig_ the sig that needs to be typed
     * @param moduleInfo_ the ModuleInfo for the focus module
     */
    private static void _createTypeForSig(Signature sig_, ModuleInfo moduleInfo_) {
       
	SigExprs superSigs;
	ModuleInfo modInfo = _moduleInfoForSig(sig_);
	if (sig_.isSubset()) {
	    sig_.setUnionType(_createUnionType(sig_));
	    superSigs = sig_.getSubsets();
	} else {
	    // check that there are no attempted to extend
	    // a subtype
	    superSigs = sig_.getExtends();
	    if (superSigs.getSigExprIter().hasNext() && 
		_getSignatureObject((SigExpr)superSigs.getSigExprIter().next(), 
				    modInfo).isSubset()) {
		Dbg.user(new Msg("Signature " + sig_.getName() + 
				 " cannot extend a subset.", sig_));
		return;
	    }
	    sig_.setSigType(_createBasicSigType(sig_));
	}
       
	// assign types to SigExprs that form the supertype or superset
	// of sig_, if any
	/**
	while (superIter.hasNext()) {
	    SigExpr curSuper = (SigExpr) superIter.next();
	    curSuper.setType(_getSignatureObject(curSuper, modInfo).getUnionType());
	    } **/
	try {
	ExprTypeCheckVisitor.typecheckNode(superSigs, 
					   modInfo, new LocalScope());
	} catch (ExprTypeCheckVisitor.TypeCheckException tce) {}
    }

    /**
     * create a union type for a signature which has no
     * type parameters, doesn't extend another signature, and
     * is a subset of a union of one or more signatures
     * @param sig_ the Signature
     * @return the UnionType
     */
    private static UnionType _createUnionType(Signature sig_) {
	Iterator superIter = sig_.getSubsets().getSigExprIter();
	ModuleInfo info = _moduleInfoForSig(sig_);
	UnionType utype = UnionType.empty(1);
	while (superIter.hasNext()) {
	    // get a superset
	    Signature superset = _getSignatureObject((SigExpr) superIter.next(), info);
	    //System.out.println("sig " + sig_ + " superset " + superset);
	    Dbg.chk(superset.getUnionType() != null, "attempted to type subset before superset");
	    // add the union type of the superset to the union type of sig_.
	    // NOTE:  this is necessary because signatures are allowed to be "in" signatures that
	    // are themselves subsets.
	    utype = utype.union(superset.getUnionType());
	    
	}
	return utype;
    }

    /**
     * create a sig type for a signature which doesn't extend
     * another signature
     * @param sig_ the Signature
     * @param typeParams_ the list of type parameters (BasicTypes) for sig_, if any 
     * @return the SigType
     */
    private static SigType _createBasicSigType(Signature sig_) {
        Dbg.check(!SigType.hasSigType(sig_), "type exists for basic sig type");
	return SigType.getGlobalSigType(sig_);
    }

    
    private static ModuleInfo _moduleInfoForSig(Signature sig_) {
        ModuleInfo moduleInfo = ((Module)sig_.getParent().getParent()).getModuleInfo();
        return moduleInfo;
    }
        
    /**
     * get the Signature object for a SigExpr
     * @param sigExpr_ the SigExpr
     * @param moduleScope_ the ModuleScope
     * @return the Signature
     */
    private static Signature _getSignatureObject(SigExpr sigExpr_, ModuleInfo moduleScope_) {
        QualifiedName extSigName = sigExpr_.getSig();
        Signature extSig = moduleScope_.getSignature(extSigName, "");
        Dbg.chk(extSig);
        return extSig;
    }

    /**
     * get the Signature object for a sig name
     * @param sigName_ name of the sig
     * @param moduleScope_ the ModuleScope
     * @return the Signature or null if no signature with sigName_ exists in moduleScope_
     */
    private static Signature _getSignatureObject(String sigName_, ModuleInfo moduleScope_) {
	Signature ret = null;
	try {
	    ret = (Signature) moduleScope_.getParagraph(sigName_);
	} 
	catch (ModuleInfo.MultipleMappingsException mme) {} // do nothing
	catch (ModuleInfo.NoParagraphException npe) {} // do nothing
	catch (ClassCastException cce) {} // do nothing
	return ret;
	
    }

    private static class InvalidDeclException extends Exception {}

    private abstract static class SigTest {

        public Object _testObject;

        public SigTest(Object testObject_) {
            _testObject = testObject_;
        }

        public abstract void test(SigExpr sigExpr_, ModuleInfo moduleInfo_) throws InvalidDeclException;
    }
}

